topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
fiber space, space attachment
Extra stuff, structure, properties
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
continuous metric space valued function on compact metric space is uniformly continuous
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
The fan theorem is one of the basic principles of intuitionism that make it more specific (even in mathematical practice, independent of any philosophical issues) than garden-variety constructive mathematics. Its main use is to justify pointwise analysis; without it, one really needs locale theory for point-free topology instead. In classical mathematics, the fan theorem is true.
Consider the finite and infinite sequences of binary digits. Given an infinite sequence and a natural number , let be the finite sequence consisting of the first elements of .
Let be a collection of finite sequences of bits (or bitlists), that is a subset of the free monoid on the boolean domain. Given an infinite sequence and a natural number , we say that -bars if ; given only , we say that bars if -bars for some .
We are interested in these three properties of :
A bar is a barred subset .
Every decidable bar is uniform. (In other words, if a collection of bitlists is decidable and barred, then it is also uniform.)
Every bar is uniform. (In other words, if a collection of bitlists is barred, then it is also uniform.)
Although the fan theorem is about bars, it is different from the bar theorem, also known as “bar induction”, which is related but stronger. The fan theorem discusses bars on lists of elements of ; the bar theorem discusses bars on lists of elements of .
Bar induction has three forms; decidable bar induction, monotone bar induction, and full bar induction (each stronger than the previous). The decidable fan theorem follows from decidable bar induction; the full fan theorem follows from monotone bar induction. Full bar induction, the strongest of the three, is a classical theorem; however, full bar induction implies Bishop’s limited principle of omniscience. Kleene's second realizability model provides a model of monotone bar induction plus Brouwer’s continuity principle.
Let be the set of binary digits (bits) and the set of natural numbers (numbers). Given a set , let be the set of finite sequences of elements of , let be the set of infinite sequences of elements of , and let be the set of decidable subsets of . Then the fan theorem is about (elements of) , , and .
However, the sets , , and are all isomorphic. Similarly, the sets , , , and are all isomorphic. In much of the literature on bars, one tacitly uses all of these isomorphisms, taking and as chosen representatives of their isomorphism classes. Thus, everything in sight is either a natural number or an infinite sequence of bits.
The fan theorem is hard enough to understand when is an infinite sequence of bits and is a finite sequence of bits; it is even harder to understand when is a natural number that bears no immediate relationship to the digits in the sequence .
In classical mathematics, the fan theorem is simply true.
In constructive mathematics, the full fan theorem is equivalent to any and all of the following statements:
Assuming some amount of countable/dependent choice (probably pretty weak: haven’t checked myself though), the full fan theorem is equivalent to each of the following statements:
However, some of these equivalences fail in the absence of countable choice. See
which shows that the compactness of does not necessarily imply the fan theorem constructively if one does not have some amount of countable choice available.
The decidable fan theorem (assuming some amount of countable/dependent choice) is equivalent to any of the following statements:
For the above equivalences with the decidable fan theorem, see
The above paper unfortunately uses different terminology than this article; for example, using “branch-bounded” and “bounded” in place of “barred” and “uniform”. The above paper also proves that, assuming all functions are computable, there exists a decidable bar which is not uniform (and, as the title suggests, a uniformly continuous function whose range has an infimum of zero).
Some form of the fan theorem follows from any of these statements (some work needs to be done to verify these and get citations):
I need to figure out how it relates to the various versions of König's Lemma?, as well as these statements (which are mutually equivalent):
Some of the results above may use countable choice, but probably no more than (which is choice for relations between and itself).
Point-wise real analysis without the fan theorem is very difficult, as shown by the example above from Waaldijk regarding “kontinuous” functions: without the fan theorem there isn’t really even a good notion of continuity! This was Brouwer's motivation for introducing the fan theorem.
However, the fan theorem (and bar theorem) can be avoided by instead using locales or another point-free approach to analysis.
Fourman and Hyland prove that the Fan theorem is true for all toposes of sheaves on a topological space, while also providing a sheaf model not satisfying the fan theorem. In other words, for Localic toposes, the underlying locale being spatial implies that the internal locale of real numbers is spatial, and that the internal cantor locale is spatial.
The reference also proves that sheaf toposes over locally countably compact topological spaces satisfy the stronger bar theorem.
I should write down the classical proof (which uses excluded middle), as well as Brouwer's argument.
Ideally, the page on bar induction would contain the classical proof of full bar induction, as well as Brouwer’s reasoning for why bar induction should hold. We would then provide constructive proofs here that monotone bar induction implies the full fan theorem, and that decidable bar induction implies the decidable fan theorem.
Thanks to Giovanni Curi on constructive news.
Frank Waaldijk pointed out exactly why point-wise analysis needs the fan theorem.
I need to read the relevant parts here:
More links that I need to keep in mind:
Also:
Last revised on August 22, 2024 at 03:40:28. See the history of this page for a list of all contributions to it.